\begin{context}[h]
{\small
\begin{verbatim}
/*******************************
Context ListStr
for strings and list of strings programs
********************************/

TyList = TT X . X -> (String->X->X)->X;
TyBool = TT X . X -> X ->X;

true = Lam X . lam x : X . lam y : X . x;
false = Lam X . lam x : X . lam y : X . y;

empty_list  =   Lam X . lam x : X . lam y : String->X->X . x;
cons        =   lam elt : String .
                lam lst : TyList .
                Lam X . lam x : X . lam y : String->X->X . y elt (lst [X] x y);

empty_string = "";

length : String->Int;
concat : String->String->String;
compstr : String -> String -> TyBool;
substr : String -> Int -> Int -> String;
\end{verbatim}}
\caption{$ListStr$, a context for evolving list operations}\label{ListStr}
\end{context}
\noindent A {\em context}, such as the one displayed in
\ref{ListStr} contains the necessary information needed to read a
term. The typing
relationships of \SF{} cannot be represented in Backus-Naur form, thus, the use of
\SF{} as a representation scheme requires the use of a context which
is simply a list of indexed names associated with relevant
information. The formal definition of a context is below:
\begin{definition}[Context]
\begin{verbatim}

    Context ::= (<String> * <Binding>) list
\end{verbatim}
\end{definition}
\noindent
In which the object of type binding contains the relevant information needed to use the name appropriately. Each term is associated with a context, and when a term contains abstractions, the context associated with the inner sub-terms (inner contexts) of the term are extensions of the outer context that include additional elements corresponding to the variables (types or typed term variables) that exist within the scope of the inner term. For example, in the term of \ref{outer_context_term23},
\begin{equation}\label{outer_context_term23}
    \underbrace{\lambda x^{Int} . \overbrace{\lambda y^{Int} . \overbrace{plus\ x\ y}^{\text{context 3 (innermost)}}}^{\text{context 2}}}_{\text{context 1 (outermost)}}
\end{equation}
a suitable outer context to represent this term would need to contain (at a minimum) the symbol
$plus$ and its type, $\typ{\AT{Int}{\AT{Int}{Int}}}$. Context 2, the context for the $(\lambda y^{Int} . plus\ x\ y)$
part of term \ref{outer_context_term23} is the outermost context extended with the variable $x:Int$.
Context 3, the context associated with the $(plus\ x\ y)$  sub-term is context 2 extended with the variable $y:Int$.
We pre-included the types $Unit$, $Int$, $String$ and $Float$ into the system. ``Pre-including" in this case
means that these types and their objects are part of the underlying implementation rather than of the
representation scheme. The definitions that are normally provided to a GP system through its terminal set are also provided
via the context. The context file is translated to a list of names and their associated definition. For example, in our implementation, context \ref{ListStr} is stored into something similar to the following list (with the context indexes on the left):
{\small
\begin{verbatim}
index   Name           Binding
0       substr:         Term constant of type String-> Int-> Int-> String
1       compstr:        Term constant of type String-> String-> TyBool
2       concat:         Term constant of type String-> String-> String
3       length:         Term constant of type String-> Int
4       empty_string:   Name For Composed Term ""
5       cons:           Name For Composed Term lam d:String.lam d':TyList.
                        ...Lam K.lam s:K.lam f:String-> K-> K.f d (d' [K] s f)
6       empty_list:     Name For Composed Term Lam V.lam j:V.lam h:String-> V-> V.j
7       false:          Name For Composed Term Lam J.lam v:J.lam y:J.y
8       true:           Name For Composed Term Lam L.lam p:L.lam r:L.p
9       TyBool:         Name For Composed Type TT A. A-> A-> A
10      TyList:         Name For Composed Type TT X. X-> (String-> X-> X)-> X
\end{verbatim}}
\noindent
The names defined in a context may refer to objects that exist outside \SF{} or to constructs that exist within it. Unlike other GP representation systems, in which primitives are only names for the functions and terminals used to construct genotypes, in an \ABGPS, primitives may also be used to encode known information about the relationships that exist within the solution space. The information relevant to the each primitive is stored in the binding object associated with its name. Primitives may be:
    \begin{enumerate}
    \item {\em Atomic types}, used as names for sets of objects. For example, the types $\typ{Food}$, $\typ{Obstacle}$ or $\typ{Behavior}$.
    \item {\em Names for Composite Types}, used to describe concepts related to the problem. For example, defining the type $\typ{Object}$ as:
    \begin{equation}\label{ObjectType}
    \ObjectType
    \end{equation}
    indicates that an object of type $\typ{Object}$ may be either an object of type $\typ{Food}$, $\typ{Obstacle}$ or $\typ{Pheromone}$. Some types may be included as either atomic or composite. For example, the type $\typ{Boolean}$ might be included as a name for the type $\typ{\Pi X.\AT{X}{\AT{X}{X}}}$ or as an atomic type. The system's user may also choose to include some composite types as a mechanism to simplify expressions. For example, the type $\typ{\AT{\Num}{\AT{\Num}{\Num}}}$ might be renamed as the shorter $\typ{BiOp}$.
    \item {\em Typed free variables} are used to define or name concepts with an execution or evaluation procedure outside \SF{} normalization. Free variables are included in \polyTypedTerminalSet{} in the form $(\alpha:\Gamma)$, with $\Gamma$ the type of the variable $\alpha$. For example, $(6:\typ{\Num})$, $(plus:\typ{BiOp})$, $(move : \typ{\AT{Direction}{Behavior}})$ or $(north : \typ{Direction})$
    \item {\em Names for \SF{} terms}, the types of which need not be included as they can be inferred by the system.
           For example, in table \ref{sideEffectABGPTypedTerminalsBetterTyped}, $true$ is included as a name for the
           term $(\Lambda X. \lambda x^{X}. \lambda y^X. x)$ and $detectFood$ as a name for the term
           \begin{equation*}
           \begin{split}
           \lambda d^{Direction}.&(cell\ d)\ \typ{Boolean}\\
                & false\\
                &(\la{o}{Object}.o\ [Boolean]\ (\la{f}{Food}.true)\ (\la{o}{Obstacle}.false)\ (\la{p}{Pheromone}.false)))
            \end{split}
            \end{equation*}
            \noindent
           making $detectFood$ an object of type $\typ{\AT{Direction}{Boolean}}$
           with $cell$ defined as the free variable
           \begin{equation*}
           (cell: \typ{\AT{Direction}{(\Pi X. \AT{X}{\AT{(\AT{Object}{X})}{X}})}})
           \end{equation*}
           and $\typ{Object}$ defined as in \ref{ObjectType}. The type $\typ{\Pi X. \AT{X}{\AT{(\AT{Object}{X})}{X}}}$ represents a structure that may contain nothing or an object of type $\typ{Object}$.
    \end{enumerate}
    Tables \ref{sideEffectABGPTypedTerminalsBetterTyped} and \ref{tab:ctxex1} contain two  sample context files (with expressions represented using mathematical notation).


  \begin{context}[h]
    \begin{small}
    \begin{center}
    \begin{tabular}{|l|l|}
    \hline\hline
    {\bf Type} & {\bf }\\
    \hline\hline
    $\typ{Behavior}$ & User Defined Atomic Type (UDAT) \\ \hline
    $\typ{Obstacle}$ & User Defined Atomic Type (UDAT) \\ \hline
    $\typ{Food}$ & User Defined Atomic Type (UDAT) \\ \hline
    $\typ{Pheromone}$ & User Defined Atomic Type (UDAT) \\ \hline
    $\typ{Direction}$ & User Defined Atomic Type (UDAT)\\
    \hline\hline
    {\bf Type Name} & {\bf Type}\\
    \hline\hline
    $\typ{Object}$ & $\ObjectType$ \\
    $\typ{Boolean}$ & $\typ{\Pi X. \AT{X}{\AT{X}{X}}}$ \\
    \hline\hline
    {\bf Functions} & {\bf Type}\\
    \hline\hline
    $cell$ & $\typ{\AT{Direction}{(\Pi X.\AT{X}{\AT{(\AT{Object}{X})}{X}})}}$\\ \hline
    $dropPheromone$ & $\typ{Behavior}$\\ \hline
    $move$ & $\typ{\AT{Direction}{Behavior}}$\\ \hline
    $turn$ & $\typ{\AT{Direction}{Behavior}}$\\ \hline
    $pickUpFood$ & $\typ{\AT{Food}{Behavior}}$\\ \hline
    {\bf Term Name} & {\bf Term}\\
    \hline\hline
    $true$ & $\Lambda X.\la{x}{X}.\la{y}{Y}.x$\\
    $false$ & $\Lambda X.\la{x}{X}.\la{y}{Y}.y$\\
    $detectFood$ & \tiny{$(\lambda d^{Direction}.(cell\ d)\ \typ{Boolean} \ false\ (\la{o}{Object}.o\ [Boolean]\ (\la{f}{Food}.true)\ (\la{o}{Obstacle}.false)\ (\la{p}{Pheromone}.false)))$}\\
    $detectPheromone$ & \tiny{$(\lambda d^{Direction}.(cell\ d)\ \typ{Boolean} \ false\ (\la{o}{Object}.o\ [Boolean]\ (\la{f}{Food}.false)\ (\la{o}{Obstacle}.false)\ (\la{p}{Pheromone}.true)))$}\\ \hline\hline
    {\bf Terminals} & {\bf Type}\\
    \hline\hline
    $front$ & $\typ{Direction}$\\ \hline
    $left$ & $\typ{Direction}$ \\ \hline
    $right$ & $\typ{Direction}$ \\ \hline\hline
    \end{tabular}
    \caption{An example context for a sample side-effect ABGP system}
    \label{sideEffectABGPTypedTerminalsBetterTyped}
    \end{center}
    \end{small}
    \end{context}

%\begin{definition}[Type Terminals]
%Let $ty$ be a set of symbols (beginning with an upper-case first letter, for clarity).
%A type $\sigma$ is either an element of $ty$, a construct of the form $\AT{\alpha}{\beta}$
%where $\alpha$ and $\beta$ are types on $ty$ or a construct of the form $\Pi X . \beta$ where
%$\beta$ is a type on $ty\cup\{X\}$. Let $ty_p$ be a set of names for types on $ty$.
%
%    \end{definition}
  \begin{context}[h]
    \begin{small}
    \begin{center}
    \begin{tabular}{l|l|l|}
    \hline\hline
    {\bf Index}&{\bf Function Name} & {\bf Type}\\
    \hline\hline
    0 & $gt$ & $\typ{\AT{TyInt}{\AT{TyInt}{(\Pi X.\AT{X}{\AT{X}{X}})}}}$\\
    1 & $plus$ & $\typ{\AT{TyInt}{\AT{TyInt}{TyInt}}}$\\
    2 & $div$ & $\typ{\AT{TyInt}{\AT{TyInt}{TyInt}}}$\\
    3 & $minus$ & $\typ{\AT{TyInt}{\AT{TyInt}{TyInt}}}$\\
    4 & $times$ & $\typ{\AT{TyInt}{\AT{TyInt}{TyInt}}}$\\
    \hline\hline
    {\bf Index} & {\bf Terminal Name} & {\bf Type}\\
    \hline\hline
    5 & $time$ & $\typ{TyInt}$\\
    6 & $zero$ & $\typ{TyInt}$\\
    7 & $one$ & $\typ{TyInt}$\\
    \hline\hline
    \end{tabular}
    \caption{A context for a sample value ABGP system}
    \label{tab:ctxex1}
    \end{center}
    \end{small}
    \end{context}
